Termination w.r.t. Q proof of /tmp/tmpFnEoOv/qsort.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

Q restricted rewrite system:
The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

Q is empty.

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → APPEND(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))
QSORT(cons(x, xs)) → FILTERLOW(x, cons(x, xs))
QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → FILTERHIGH(x, cons(x, xs))
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
FILTERLOW(n, cons(x, xs)) → GE(n, x)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
FILTERHIGH(n, cons(x, xs)) → GE(x, n)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
GE(s(x), s(y)) → GE(x, y)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → APPEND(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))
QSORT(cons(x, xs)) → FILTERLOW(x, cons(x, xs))
QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → FILTERHIGH(x, cons(x, xs))
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
FILTERLOW(n, cons(x, xs)) → GE(n, x)
IF1(true, n, x, xs) → FILTERLOW(n, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
FILTERHIGH(n, cons(x, xs)) → GE(x, n)
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
GE(s(x), s(y)) → GE(x, y)
APPEND(cons(x, xs), ys) → APPEND(xs, ys)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 5 SCCs with 5 less nodes.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(x, xs), ys) → APPEND(xs, ys)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(x, xs), ys) → APPEND(xs, ys)

R is empty.
The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

APPEND(cons(x, xs), ys) → APPEND(xs, ys)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

APPEND(cons(x, xs), ys) → APPEND(xs, ys)
The graph contains the following edges 1 > 1, 2 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

R is empty.
The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

GE(s(x), s(y)) → GE(x, y)

From the DPs we obtained the following set of size-change graphs:

GE(s(x), s(y)) → GE(x, y)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF2(true, n, x, xs) → FILTERHIGH(n, xs)
FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
IF2(false, n, x, xs) → FILTERHIGH(n, xs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

FILTERHIGH(n, cons(x, xs)) → IF2(ge(x, n), n, x, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF2(true, n, x, xs) → FILTERHIGH(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
IF2(false, n, x, xs) → FILTERHIGH(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

IF1(true, n, x, xs) → FILTERLOW(n, xs)
FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
IF1(false, n, x, xs) → FILTERLOW(n, xs)

The TRS R consists of the following rules:

ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)

The set Q consists of the following terms:

ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

From the DPs we obtained the following set of size-change graphs:

FILTERLOW(n, cons(x, xs)) → IF1(ge(n, x), n, x, xs)
The graph contains the following edges 1 >= 2, 2 > 3, 2 > 4
IF1(true, n, x, xs) → FILTERLOW(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2
IF1(false, n, x, xs) → FILTERLOW(n, xs)
The graph contains the following edges 2 >= 1, 4 >= 2

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))

The TRS R consists of the following rules:

qsort(nil) → nil
qsort(cons(x, xs)) → append(qsort(filterlow(x, cons(x, xs))), cons(x, qsort(filterhigh(x, cons(x, xs)))))
filterlow(n, nil) → nil
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(true, n, x, xs) → filterlow(n, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterhigh(n, nil) → nil
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(true, n, x, xs) → filterhigh(n, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
append(nil, ys) → ys
append(cons(x, xs), ys) → cons(x, append(xs, ys))

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))

The TRS R consists of the following rules:

if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil

The set Q consists of the following terms:

qsort(nil)
qsort(cons(x0, x1))
filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))
append(nil, ys)
append(cons(x0, x1), ys)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

qsort(nil)
qsort(cons(x0, x1))
append(nil, ys)
append(cons(x0, x1), ys)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))

The TRS R consists of the following rules:

if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule QSORT(cons(x, xs)) → QSORT(filterhigh(x, cons(x, xs))) at position [0] we obtained the following new rules [LPAR04]:

QSORT(cons(x, xs)) → QSORT(if2(ge(x, x), x, x, xs))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs)))
QSORT(cons(x, xs)) → QSORT(if2(ge(x, x), x, x, xs))

The TRS R consists of the following rules:

if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
By rewriting [LPAR04] the rule QSORT(cons(x, xs)) → QSORT(filterlow(x, cons(x, xs))) at position [0] we obtained the following new rules [LPAR04]:

QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(if2(ge(x, x), x, x, xs))
QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))

The TRS R consists of the following rules:

if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

This DP could be deleted by the Induction-Processor:
QSORT(cons(x', xs')) → QSORT(if2(ge(x', x'), x', x', xs'))

This order was computed:
Polynomial interpretation [POLO]:

POL(0) = 0
POL(QSORT(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₂
POL(false) = 1
POL(filterhigh(x₁, x₂)) = x₂
POL(filterlow(x₁, x₂)) = x₂
POL(ge(x₁, x₂)) = 1
POL(if1(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(if2(x₁, x₂, x₃, x₄)) = x₁ + x₄
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

At least one of these decreasing rules is always used after the deleted DP:
ge(x18', 0) → true

The following formula is valid:
x':sort[a0],xs':sort[a2].(if2'(ge(x' , x' ), x' , x' , xs' )=true∨ge'(x' , x' )=true)

The transformed set:
if1'(true, n', x', xs') → filterlow'(n', xs')
filterlow'(n7, cons(x8, xs5)) → if1'(ge(n7, x8), n7, x8, xs5)
ge'(x18, 0) → true
ge'(0, s(x28)) → false
ge'(s(x38), s(y2)) → ge'(x38, y2)
if1'(false, n40, x48, xs30) → filterlow'(n40, xs30)
filterlow'(n49, nil) → false
if2'(true, n58, x67, xs43) → filterhigh'(n58, xs43)
filterhigh'(n67, cons(x77, xs50)) → or(if2'(ge(x77, n67), n67, x77, xs50), ge'(x77, n67))
if2'(false, n76, x87, xs57) → filterhigh'(n76, xs57)
filterhigh'(n85, nil) → false
if1(true, n', x', xs') → filterlow(n', xs')
filterlow(n7, cons(x8, xs5)) → if1(ge(n7, x8), n7, x8, xs5)
ge(x18, 0) → true
ge(0, s(x28)) → false
ge(s(x38), s(y2)) → ge(x38, y2)
if1(false, n40, x48, xs30) → cons(x48, filterlow(n40, xs30))
filterlow(n49, nil) → nil
if2(true, n58, x67, xs43) → filterhigh(n58, xs43)
filterhigh(n67, cons(x77, xs50)) → if2(ge(x77, n67), n67, x77, xs50)
if2(false, n76, x87, xs57) → cons(x87, filterhigh(n76, xs57))
filterhigh(n85, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a2](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a2](x0, x2), equal_sort[a2](x1, x3))
equal_sort[a2](cons(x0, x1), nil) → false
equal_sort[a2](nil, cons(x0, x1)) → false
equal_sort[a2](nil, nil) → true
equal_sort[a55](witness_sort[a55], witness_sort[a55]) → true

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                    ↳ QTRS

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))

The TRS R consists of the following rules:

if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
ge(x, 0) → true
ge(0, s(x)) → false
ge(s(x), s(y)) → ge(x, y)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
if2(true, n, x, xs) → filterhigh(n, xs)
filterhigh(n, cons(x, xs)) → if2(ge(x, n), n, x, xs)
if2(false, n, x, xs) → cons(x, filterhigh(n, xs))
filterhigh(n, nil) → nil

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                    ↳ QTRS

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))

The TRS R consists of the following rules:

ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

filterhigh(x0, nil)
filterhigh(x0, cons(x1, x2))
if2(true, x0, x1, x2)
if2(false, x0, x1, x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Induction-Processor

                                    ↳ QTRS

Q DP problem:
The TRS P consists of the following rules:

QSORT(cons(x, xs)) → QSORT(if1(ge(x, x), x, x, xs))

The TRS R consists of the following rules:

ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.

This DP could be deleted by the Induction-Processor:
QSORT(cons(x', xs')) → QSORT(if1(ge(x', x'), x', x', xs'))

This order was computed:
Polynomial interpretation [POLO]:

POL(0) = 0
POL(QSORT(x₁)) = x₁
POL(cons(x₁, x₂)) = 1 + x₂
POL(false) = 0
POL(filterlow(x₁, x₂)) = x₂
POL(ge(x₁, x₂)) = 0
POL(if1(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(nil) = 0
POL(s(x₁)) = 0
POL(true) = 0

At least one of these decreasing rules is always used after the deleted DP:
if1(true, n60, x120, xs40) → filterlow(n60, xs40)

The following formula is valid:
x':sort[a0],xs':sort[a5].if1'(ge(x' , x' ), x' , x' , xs' )=true

The transformed set:
if1'(true, n6, x12, xs4) → true
filterlow'(n11, cons(x19, xs8)) → if1'(ge(n11, x19), n11, x19, xs8)
if1'(false, n16, x26, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge(x', 0) → true
ge(s(x5), s(y'')) → ge(x5, y'')
if1(true, n6, x12, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x19, xs8)) → if1(ge(n11, x19), n11, x19, xs8)
if1(false, n16, x26, xs12) → cons(x26, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x39)) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a36](witness_sort[a36], witness_sort[a36]) → true

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Induction-Processor

                                                ↳ AND

                                                  ↳ QDP

                                                    ↳ PisEmptyProof

                                                  ↳ QTRS

                                    ↳ QTRS

Q DP problem:
P is empty.
The TRS R consists of the following rules:

ge(x, 0) → true
ge(s(x), s(y)) → ge(x, y)
if1(true, n, x, xs) → filterlow(n, xs)
filterlow(n, cons(x, xs)) → if1(ge(n, x), n, x, xs)
if1(false, n, x, xs) → cons(x, filterlow(n, xs))
filterlow(n, nil) → nil
ge(0, s(x)) → false

The set Q consists of the following terms:

filterlow(x0, nil)
filterlow(x0, cons(x1, x2))
if1(true, x0, x1, x2)
if1(false, x0, x1, x2)
ge(x0, 0)
ge(0, s(x0))
ge(s(x0), s(x1))

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Induction-Processor

                                                ↳ AND

                                                  ↳ QDP

                                                  ↳ QTRS

                                                    ↳ QTRSRRRProof

                                    ↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

if1'(true, n6, x12, xs4) → true
filterlow'(n11, cons(x19, xs8)) → if1'(ge(n11, x19), n11, x19, xs8)
if1'(false, n16, x26, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge(x', 0) → true
ge(s(x5), s(y'')) → ge(x5, y'')
if1(true, n6, x12, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x19, xs8)) → if1(ge(n11, x19), n11, x19, xs8)
if1(false, n16, x26, xs12) → cons(x26, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x39)) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a36](witness_sort[a36], witness_sort[a36]) → true

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

if1'(true, n6, x12, xs4) → true
filterlow'(n11, cons(x19, xs8)) → if1'(ge(n11, x19), n11, x19, xs8)
if1'(false, n16, x26, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge(x', 0) → true
ge(s(x5), s(y'')) → ge(x5, y'')
if1(true, n6, x12, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x19, xs8)) → if1(ge(n11, x19), n11, x19, xs8)
if1(false, n16, x26, xs12) → cons(x26, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x39)) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a36](witness_sort[a36], witness_sort[a36]) → true

Q is empty.
Used ordering:
Combined order from the following AFS and order.
if1'(x1, x2, x3, x4) = if1'(x1, x2, x3, x4)
true = true
filterlow'(x1, x2) = filterlow'(x1, x2)
cons(x1, x2) = cons(x1, x2)
ge(x1, x2) = ge(x1, x2)
false = false
nil = nil
0 = 0
s(x1) = x1
if1(x1, x2, x3, x4) = if1(x1, x2, x3, x4)
filterlow(x1, x2) = filterlow(x1, x2)
equal_bool(x1, x2) = equal_bool(x1, x2)
and(x1, x2) = and(x1, x2)
or(x1, x2) = or(x1, x2)
not(x1) = not(x1)
isa_true(x1) = isa_true(x1)
isa_false(x1) = isa_false(x1)
equal_sort[a0](x1, x2) = equal_sort[a0](x1, x2)
equal_sort[a5](x1, x2) = equal_sort[a5](x1, x2)
equal_sort[a36](x1, x2) = equal_sort[a36](x1, x2)
witness_sort[a36] = witness_sort[a36]

Recursive path order with status [RPO].
Quasi-Precedence:

[false, nil, 0, not₁, isa_true₁, isa_false₁] > [if1'₄, filterlow'₂] > [true, equal_sort[a0]₂] > [if1₄, filterlow₂] > cons₂
[false, nil, 0, not₁, isa_true₁, isa_false₁] > [if1'₄, filterlow'₂] > [true, equal_sort[a0]₂] > [if1₄, filterlow₂] > ge₂
or₂ > [true, equal_sort[a0]₂] > [if1₄, filterlow₂] > cons₂
or₂ > [true, equal_sort[a0]₂] > [if1₄, filterlow₂] > ge₂
equal_sort[a5]₂ > and₂
equal_sort[a36]₂ > [true, equal_sort[a0]₂] > [if1₄, filterlow₂] > cons₂
equal_sort[a36]₂ > [true, equal_sort[a0]₂] > [if1₄, filterlow₂] > ge₂

Status:

if1'₄: [4,2,1,3]
true: multiset
or₂: multiset
and₂: [2,1]
filterlow'₂: [2,1]
equal_sort[a36]₂: multiset
0: multiset
equal_bool₂: multiset
equal_sort[a0]₂: [1,2]
cons₂: [1,2]
equal_sort[a5]₂: multiset
witness_sort[a36]: multiset
not₁: multiset
isa_false₁: multiset
false: multiset
filterlow₂: [1,2]
ge₂: multiset
nil: multiset
if1₄: [2,4,3,1]
isa_true₁: [1]

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

if1'(true, n6, x12, xs4) → true
filterlow'(n11, cons(x19, xs8)) → if1'(ge(n11, x19), n11, x19, xs8)
if1'(false, n16, x26, xs12) → filterlow'(n16, xs12)
filterlow'(n21, nil) → false
ge(x', 0) → true
if1(true, n6, x12, xs4) → filterlow(n6, xs4)
filterlow(n11, cons(x19, xs8)) → if1(ge(n11, x19), n11, x19, xs8)
if1(false, n16, x26, xs12) → cons(x26, filterlow(n16, xs12))
filterlow(n21, nil) → nil
ge(0, s(x39)) → false
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a5](nil, nil) → true
equal_sort[a5](nil, cons(x0, x1)) → false
equal_sort[a5](cons(x0, x1), nil) → false
equal_sort[a5](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a5](x0, x2), equal_sort[a5](x1, x3))
equal_sort[a36](witness_sort[a36], witness_sort[a36]) → true

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Induction-Processor

                                                ↳ AND

                                                  ↳ QDP

                                                  ↳ QTRS

                                                    ↳ QTRSRRRProof

                                                      ↳ QTRS

                                                        ↳ QTRSRRRProof

                                    ↳ QTRS

Q restricted rewrite system:
The TRS R consists of the following rules:

ge(s(x5), s(y'')) → ge(x5, y'')
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

ge(s(x5), s(y'')) → ge(x5, y'')
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

Q is empty.
Used ordering:
Polynomial interpretation [POLO]:

POL(equal_sort[a0](x₁, x₂)) = x₁ + x₂
POL(ge(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 1 + x₁

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

ge(s(x5), s(y'')) → ge(x5, y'')
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                      ↳ UsableRulesProof

                                        ↳ QDP

                                          ↳ QReductionProof

                                            ↳ QDP

                                              ↳ Induction-Processor

                                                ↳ AND

                                                  ↳ QDP

                                                  ↳ QTRS

                                                    ↳ QTRSRRRProof

                                                      ↳ QTRS

                                                        ↳ QTRSRRRProof

                                                          ↳ QTRS

                                                            ↳ RisEmptyProof

                                                            ↳ RisEmptyProof

                                                            ↳ RisEmptyProof

                                    ↳ QTRS

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.
The TRS R is empty. Hence, termination is trivially proven.
The TRS R is empty. Hence, termination is trivially proven.

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QTRS

                                      ↳ QTRSRRRProof

Q restricted rewrite system:
The TRS R consists of the following rules:

if1'(true, n', x', xs') → filterlow'(n', xs')
filterlow'(n7, cons(x8, xs5)) → if1'(ge(n7, x8), n7, x8, xs5)
ge'(x18, 0) → true
ge'(0, s(x28)) → false
ge'(s(x38), s(y2)) → ge'(x38, y2)
if1'(false, n40, x48, xs30) → filterlow'(n40, xs30)
filterlow'(n49, nil) → false
if2'(true, n58, x67, xs43) → filterhigh'(n58, xs43)
filterhigh'(n67, cons(x77, xs50)) → or(if2'(ge(x77, n67), n67, x77, xs50), ge'(x77, n67))
if2'(false, n76, x87, xs57) → filterhigh'(n76, xs57)
filterhigh'(n85, nil) → false
if1(true, n', x', xs') → filterlow(n', xs')
filterlow(n7, cons(x8, xs5)) → if1(ge(n7, x8), n7, x8, xs5)
ge(x18, 0) → true
ge(0, s(x28)) → false
ge(s(x38), s(y2)) → ge(x38, y2)
if1(false, n40, x48, xs30) → cons(x48, filterlow(n40, xs30))
filterlow(n49, nil) → nil
if2(true, n58, x67, xs43) → filterhigh(n58, xs43)
filterhigh(n67, cons(x77, xs50)) → if2(ge(x77, n67), n67, x77, xs50)
if2(false, n76, x87, xs57) → cons(x87, filterhigh(n76, xs57))
filterhigh(n85, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a2](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a2](x0, x2), equal_sort[a2](x1, x3))
equal_sort[a2](cons(x0, x1), nil) → false
equal_sort[a2](nil, cons(x0, x1)) → false
equal_sort[a2](nil, nil) → true
equal_sort[a55](witness_sort[a55], witness_sort[a55]) → true

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

if1'(true, n', x', xs') → filterlow'(n', xs')
filterlow'(n7, cons(x8, xs5)) → if1'(ge(n7, x8), n7, x8, xs5)
ge'(x18, 0) → true
ge'(0, s(x28)) → false
ge'(s(x38), s(y2)) → ge'(x38, y2)
if1'(false, n40, x48, xs30) → filterlow'(n40, xs30)
filterlow'(n49, nil) → false
if2'(true, n58, x67, xs43) → filterhigh'(n58, xs43)
filterhigh'(n67, cons(x77, xs50)) → or(if2'(ge(x77, n67), n67, x77, xs50), ge'(x77, n67))
if2'(false, n76, x87, xs57) → filterhigh'(n76, xs57)
filterhigh'(n85, nil) → false
if1(true, n', x', xs') → filterlow(n', xs')
filterlow(n7, cons(x8, xs5)) → if1(ge(n7, x8), n7, x8, xs5)
ge(x18, 0) → true
ge(0, s(x28)) → false
ge(s(x38), s(y2)) → ge(x38, y2)
if1(false, n40, x48, xs30) → cons(x48, filterlow(n40, xs30))
filterlow(n49, nil) → nil
if2(true, n58, x67, xs43) → filterhigh(n58, xs43)
filterhigh(n67, cons(x77, xs50)) → if2(ge(x77, n67), n67, x77, xs50)
if2(false, n76, x87, xs57) → cons(x87, filterhigh(n76, xs57))
filterhigh(n85, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a2](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a2](x0, x2), equal_sort[a2](x1, x3))
equal_sort[a2](cons(x0, x1), nil) → false
equal_sort[a2](nil, cons(x0, x1)) → false
equal_sort[a2](nil, nil) → true
equal_sort[a55](witness_sort[a55], witness_sort[a55]) → true

Q is empty.
Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:

0 > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > ge'₂ > [ge₂, and₂, equal_sort[a0]₂]
0 > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > or₂ > [ge₂, and₂, equal_sort[a0]₂]
s₁ > [if1'₄, filterlow'₂, false, if1₄, filterlow₂] > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > ge'₂ > [ge₂, and₂, equal_sort[a0]₂]
s₁ > [if1'₄, filterlow'₂, false, if1₄, filterlow₂] > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > or₂ > [ge₂, and₂, equal_sort[a0]₂]
nil > [if1'₄, filterlow'₂, false, if1₄, filterlow₂] > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > ge'₂ > [ge₂, and₂, equal_sort[a0]₂]
nil > [if1'₄, filterlow'₂, false, if1₄, filterlow₂] > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > or₂ > [ge₂, and₂, equal_sort[a0]₂]
not₁ > [if1'₄, filterlow'₂, false, if1₄, filterlow₂] > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > ge'₂ > [ge₂, and₂, equal_sort[a0]₂]
not₁ > [if1'₄, filterlow'₂, false, if1₄, filterlow₂] > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > or₂ > [ge₂, and₂, equal_sort[a0]₂]
isa_true₁ > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > ge'₂ > [ge₂, and₂, equal_sort[a0]₂]
isa_true₁ > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > or₂ > [ge₂, and₂, equal_sort[a0]₂]
isa_false₁ > [if1'₄, filterlow'₂, false, if1₄, filterlow₂] > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > ge'₂ > [ge₂, and₂, equal_sort[a0]₂]
isa_false₁ > [if1'₄, filterlow'₂, false, if1₄, filterlow₂] > [true, equal_bool₂, witness_sort[a55]] > [if2₄, filterhigh₂] > [cons₂, if2'₄, filterhigh'₂] > or₂ > [ge₂, and₂, equal_sort[a0]₂]
equal_sort[a2]₂ > [ge₂, and₂, equal_sort[a0]₂]
equal_sort[a55]₂ > [ge₂, and₂, equal_sort[a0]₂]

Status:

if2₄: [2,4,1,3]
or₂: multiset
if1'₄: [4,2,3,1]
and₂: [1,2]
equal_sort[a2]₂: [1,2]
filterlow'₂: [2,1]
equal_sort[a0]₂: multiset
not₁: [1]
isa_false₁: [1]
s₁: [1]
if1₄: [4,2,3,1]
nil: multiset
isa_true₁: [1]
ge'₂: [1,2]
filterhigh₂: [1,2]
filterhigh'₂: [2,1]
true: multiset
witness_sort[a55]: multiset
if2'₄: [4,2,3,1]
0: multiset
equal_bool₂: [2,1]
cons₂: [2,1]
filterlow₂: [2,1]
false: multiset
equal_sort[a55]₂: multiset
ge₂: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

if1'(true, n', x', xs') → filterlow'(n', xs')
filterlow'(n7, cons(x8, xs5)) → if1'(ge(n7, x8), n7, x8, xs5)
ge'(x18, 0) → true
ge'(0, s(x28)) → false
ge'(s(x38), s(y2)) → ge'(x38, y2)
if1'(false, n40, x48, xs30) → filterlow'(n40, xs30)
filterlow'(n49, nil) → false
if2'(true, n58, x67, xs43) → filterhigh'(n58, xs43)
filterhigh'(n67, cons(x77, xs50)) → or(if2'(ge(x77, n67), n67, x77, xs50), ge'(x77, n67))
if2'(false, n76, x87, xs57) → filterhigh'(n76, xs57)
filterhigh'(n85, nil) → false
if1(true, n', x', xs') → filterlow(n', xs')
filterlow(n7, cons(x8, xs5)) → if1(ge(n7, x8), n7, x8, xs5)
ge(x18, 0) → true
ge(0, s(x28)) → false
ge(s(x38), s(y2)) → ge(x38, y2)
if1(false, n40, x48, xs30) → cons(x48, filterlow(n40, xs30))
filterlow(n49, nil) → nil
if2(true, n58, x67, xs43) → filterhigh(n58, xs43)
filterhigh(n67, cons(x77, xs50)) → if2(ge(x77, n67), n67, x77, xs50)
if2(false, n76, x87, xs57) → cons(x87, filterhigh(n76, xs57))
filterhigh(n85, nil) → nil
equal_bool(true, false) → false
equal_bool(false, true) → false
equal_bool(true, true) → true
equal_bool(false, false) → true
and(true, x) → x
and(false, x) → false
or(true, x) → true
or(false, x) → x
not(false) → true
not(true) → false
isa_true(true) → true
isa_true(false) → false
isa_false(true) → false
isa_false(false) → true
equal_sort[a0](0, 0) → true
equal_sort[a0](0, s(x0)) → false
equal_sort[a0](s(x0), 0) → false
equal_sort[a0](s(x0), s(x1)) → equal_sort[a0](x0, x1)
equal_sort[a2](cons(x0, x1), cons(x2, x3)) → and(equal_sort[a2](x0, x2), equal_sort[a2](x1, x3))
equal_sort[a2](cons(x0, x1), nil) → false
equal_sort[a2](nil, cons(x0, x1)) → false
equal_sort[a2](nil, nil) → true
equal_sort[a55](witness_sort[a55], witness_sort[a55]) → true

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

              ↳ QDP

                ↳ UsableRulesProof

                  ↳ QDP

                    ↳ QReductionProof

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Induction-Processor

                                  ↳ AND

                                    ↳ QDP

                                    ↳ QTRS

                                      ↳ QTRSRRRProof

                                        ↳ QTRS

                                          ↳ RisEmptyProof

                                          ↳ RisEmptyProof

                                          ↳ RisEmptyProof